natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory
In dependent type theory, the type of classes relative to a Tarski universe is the function type from the material cumulative hierarchy higher inductive type constructed from to the type of -small h-propositions.
Let be a Tarski universe. The cumulative hierarchy relative to is the higher inductive type generated by the following:
A function
An equivalence
A set-truncator
The type of all -small propositions is defined as
The type of classes relative to is the function type , and a class relative to is just a function .
The type of classes provides a general model of material class theory.
The type of classes is defined in section 10.5.3 of:
Last revised on November 19, 2022 at 10:38:50. See the history of this page for a list of all contributions to it.